
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Utils.Provenance</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Utils.Provenance" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Utils.Provenance</h1>
<div class="coq">
<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.ZArith.ZArith.html">ZArith</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="Provenance">Provenance</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Record</span> <span class="id"><a name="location_point">location_point</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="mkLocationPoint">mkLocationPoint</a></span> {<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="offset">offset</a></span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="line">line</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="column">column</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}.<br/>
&nbsp;&nbsp;<span class="kwd">Record</span> <span class="id"><a name="location">location</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="mkLocation">mkLocation</a></span> {<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="loc_file">loc_file</a></span>: <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="loc_start">loc_start</a></span>: <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location_point">location_point</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="loc_end">loc_end</a></span>: <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location_point">location_point</a></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="dummy_location">dummy_location</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">dummy_location_point</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#mkLocationPoint">mkLocationPoint</a></span> (-1) (-1) (-1) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#mkLocation">mkLocation</a></span> "" <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_location_point">dummy_location_point</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_location_point">dummy_location_point</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Inductive</span> <span class="id"><a name="provenance">provenance</a></span> :=<br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvFunc">ProvFunc</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>   <span class="docright">(* Compiled from function  *)</span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvClause">ProvClause</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> <span class="docright">(* Compiled from clause  *)</span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvThisContract">ProvThisContract</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>     <span class="docright">(* Compiled from <span class="bracket"><span class="id">contract</span></span>  *)</span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvThisClause">ProvThisClause</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>       <span class="docright">(* Compiled from <span class="bracket"><span class="id">clause</span></span>  *)</span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvThisState">ProvThisState</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>        <span class="docright">(* Compiled from <span class="bracket"><span class="id">state</span></span>  *)</span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ProvLoc">ProvLoc</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>              <span class="docright">(* Compiled from others  *)</span><br/>
&nbsp;&nbsp;.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="dummy_provenance">dummy_provenance</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvLoc">ProvLoc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_location">dummy_location</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="loc_of_provenance">loc_of_provenance</a></span> <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#prov">prov</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvFunc">ProvFunc</a></span> <span class="id">loc</span> <span class="id">_</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvClause">ProvClause</a></span> <span class="id">loc</span> <span class="id">_</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisContract">ProvThisContract</a></span> <span class="id">loc</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisClause">ProvThisClause</a></span> <span class="id">loc</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisState">ProvThisState</a></span> <span class="id">loc</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvLoc">ProvLoc</a></span> <span class="id">loc</span> =&gt; <span class="id">loc</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_contract">is_contract</a></span> <span class="id">prov</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#prov">prov</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisContract">ProvThisContract</a></span> <span class="id">loc</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_clause">is_clause</a></span> <span class="id">prov</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#prov">prov</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisClause">ProvThisClause</a></span> <span class="id">loc</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_state">is_state</a></span> <span class="id">prov</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#prov">prov</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvThisState">ProvThisState</a></span> <span class="id">loc</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_location_point">string_of_location_point</a></span> (<span class="id">lp</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location_point">location_point</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#lp">lp</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#line">line</a></span>)) ++ ":" ++ (<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#lp">lp</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#column">column</a></span>)).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="string_of_location">string_of_location</a></span> (<span class="id">loc</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#location">location</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">f</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc">loc</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc_file">loc_file</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">file</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#f">f</a></span> ""%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> ""%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#f">f</a></span> ++ " ")%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#file">file</a></span> ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#string_of_location_point">string_of_location_point</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc">loc</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc_start">loc_start</a></span>)) ++ "-" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#string_of_location_point">string_of_location_point</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc">loc</a></span>.(<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc_end">loc_end</a></span>)).<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#Provenance">Provenance</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
